\begin{tabbing}
$M$.send($k$;$l$;$s$;$v$;${\it ms}$;$i$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(\=product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq);\+
\\[0ex]1of(2of(2of(2of(2of(2of($M$))))));
\\[0ex]$\langle$$k$$,\,$$l$$\rangle$;
\\[0ex]$k$,$L$.(\=${\it ms}$\+
\\[0ex]$=$
\\[0ex]if source($l$) = $i$$\rightarrow$ concat(map($\lambda$${\it tgf}$.map($\lambda$$x$.$\langle$1of(${\it tgf}$)$,\,$$x$$\rangle$;2of(${\it tgf}$)($s$,$v$));$L$))
\\[0ex]else nil fi
\\[0ex]$\in$ (${\it tg}$:Id$\times$if source($l$) = $i$$\rightarrow$ $M$.da(rcv($l$,${\it tg}$)) else Top fi) List))
\-\-
\end{tabbing}